$\forall$$T$:Type, $X$:MaInterface($T$ + Top). ma{-}interface{-}left($X$) $\in$ MaInterface($T$)